Electronic devices are used in a variety of products, from personal computers to automobiles to toys. There are various different types of electronic devices, such as, for example, an integrated circuit. Furthermore, as those of skill in the art will appreciate, electronic devices can be connected, to form other electronic devices or systems. The designing and fabricating of electronic devices typically involves many steps, sometimes referred to as the “design flow.” The particular steps of a design flow often are dependent upon the type of electronic device, its complexity, the design team, and the fabricator that will manufacture the device.
Several steps are common to many design flows. Initially, the specification for a new design is expressed, often in an abstract form and then transformed into lower and lower abstraction levels until the design is ultimately ready for manufacture. The process of transforming the design from one level of abstraction to another is referred to as synthesis. At several stages of the design flow, for example, after each synthesis process, the design is verified. Verification aids in the discovery of errors in the design, and allows the designers and engineers to correct or otherwise improve the design. The various synthesis and verification processes may be facilitated by electronic design automation (EDA) tools.
Synthesis and verification processes applied to modern electronic designs may be quite complex and may include many different steps. An illustrative design flow, for an integrated circuit, for example, can start with a specification for the integrated circuit being expressed in a high-level programming language, such as, for example, C++. This level of abstraction is often referred to as the algorithmic level. At this abstraction level, the functionality of the design is described in terms of the functional behavior applied to specified inputs to generate outputs. The design will then be synthesized into a lower level of abstraction, typically, one of various logic level of abstraction having different amounts of detail. At this level of abstraction, the design may expressed in a hardware description language (HDL) such as Verilog, where the circuit is described in terms of both the exchange of signals between hardware registers and the logical operations that are performed on those signals. At this stage, verification is often performed to confirm the functional behavior of the design, i.e. that the logical design conforms to the algorithmic specification.
After the logical design is verified, it is synthesized into a device design. The device design, which is typically in the form of a schematic or netlist, describes the specific electronic components (such as transistors, resistors, and capacitors) that will be used in the circuit, along with their interconnections. Verification is again performed at this stage in order to confirm that the device design conforms to the logical design, and as a result, the algorithmic specification.
Once the components and their interconnections are established, as represented by the device design, the design is again synthesized, this time into a physical design that describes specific geometric elements. The geometric elements define the shapes that will be created in various layers of material to manufacture the circuit. This type of design often is referred to as a “layout” design. The layout design is then used as a template to manufacture the integrated circuit. Verification is again performed, to ensure that the layout design conforms to the device design.
Although there are different methods of performing verification, various embodiments disclosed herein are directed towards verification processes that “exercise” a design by applying input to the design and capturing the output resulting from application of the input. The applied input is often referred to as an input vector. The captured output then is compared to the output the design should have produced according to the input vector and the specification. Various technologies exist for exercising a design. For example, the response (i.e. the output) of the design to the input vector may be simulated in software. In some cases, the output may be captured from an emulator that is emulating the design with the input vector as stimulus for the emulation. In other aspects, a prototype may also be used to generate the output. Those of ordinary skill in the art will appreciate that combinations of simulation, emulation, and prototyping could be used in various combinations during verification and that various combinations of technologies can be employed to implement a verification system as described here.
Verification, in various aspects. consists of applying multiple input vectors sequentially (where an input vector is a tuple of values for input variables,) referred to as the test set and capturing each resulting output, referred to as the output set. The individual outputs from the output set then are compared to the corresponding expected outputs. There are many ways to generate the input vectors to include in a test set. For example, directed tests, that is, where the input vectors are directly specified by a designer can be employed. Random combinations of inputs can also be selected and used to form input vectors. One could generate a test set that corresponds to all possible input combinations. The set of all possible input vectors to a modern electronic design may be so large however, that it is not computationally feasible to exhaustively test the design in this manner. As a result, another approach to generating input vectors for verification is often used.
Each input of a design has a domain. The domain specifies the set of possible values that may be applied to the input corresponding to the domain. Sometimes, there are constraints, which restrict the combinations of input values that may be used to generate an input vector. These constraints may include legality constraints (e.g., which may be derived from the design's operating specification), apparatus constraints (e.g., which may be derived from the specifications of the equipment used to exercise the design), and/or coverage constraints (e.g., which may be derived from a verification plan). Other types of constraints may also be used to limit or restrict the input values, which may be used to generate input vectors.
The process of finding a tuple of values (e.g., a vector), which satisfies a set of constraints, is often referred to as “constraint solving”. The process of finding a set of tuples of values, within which every tuple satisfies a set of constraints, is sometimes referred to as “constraint exploration.”
Conceptually, to find a solution (or a set of solutions) to a constraint set, one could iterate through the set of possible value tuples (i.e. the cross products of the domains of the variables) and test each tuple against the constraints, selecting only those tuples that satisfy every constraint, until the desired number of solutions is found. In practice, for modern electronic devices, the size of the set of possible value tuples (sometimes referred to as the “input space”) is so large and the fraction of acceptable tuples is so small that the iteration approach is not practical. Instead, computational techniques such as satisfiability analysis are used to locate acceptable tuples within the input space. Those of ordinary skill in the art will appreciate that such computational techniques generally run considerably faster if the size of the input space can be reduced. Therefore, methods that can identify solution-free regions of an input space that can be pruned without affecting the verification results are of considerable interest.
Example embodiments of the disclosure discuss methods and techniques for pruning the input space as indicated above. Although such discussion is generally made with reference to coverage constraints, those of ordinary skill in the art will appreciate that other types of constraints may be used without departing from the spirit and scope of the invention.